Semiformal verification for pipelined digital designs based on Algorithmic State Machines

The method and tools to use Algorithmic State Machine (ASM) formalism for high-level specification of complex digital designs and their Model-Checking-based verification are described. This methodology is based on the possibility of hierarchical description of the target digital designs at algorithmic level of abstraction, and ability to generate finite state machines (FSM) models of the systems from the ASM flowcharts. The software tool was developed for automatic generation of SMV (Symbolic Modes Verifier) codes from the ASMs and corresponding FSMs. A way of this approach application to design verification is demonstrated for a pipelined microprocessor.